Nuprl Lemma : atom-free-ma-ds
0,22
postcript
pdf
A
:MsgA. AtomFree(ds(
A
))
(
x
:Id. AtomFree(Type;
A
.ds(
x
)))
latex
Definitions
P
Q
,
AtomFree(
T
;
x
)
,
Type
,
AtomFree(
d
)
,
Id
,
IdDeq
,
ds(
M
)
,
x
:
A
.
B
(
x
)
,
t
T
,
MsgA
,
a
:
A
fp
B
(
a
)
,
M
.ds(
x
)
,
EqDecider(
T
)
,
product-deq(
A
;
B
;
a
;
b
)
,
proddeq(
a
;
b
)
,
prod-deq(
A
;
B
;
a
;
b
)
,
AtomDeq
,
atom-deq-aux
,
NatDeq
,
<
a
,
b
>
,
nat-deq-aux
,
f
(
a
)
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
type
List
,
x
:
A
B
(
x
)
,
Atom
,
,
{
x
:
A
|
B
(
x
) }
,
,
A
B
,
A
,
False
,
Void
,
a
<
b
,
#$n
,
x
:
A
B
(
x
)
,
f
(
x
)?
z
,
x
.
A
(
x
)
,
Top
,
x
.
t
(
x
)
Lemmas
fpf
wf
,
top
wf
,
fpf-cap
wf
,
atom-free-Id
,
atom-free-fpf
,
msga
wf
,
ma
ds
wf
,
id-deq
wf
,
Id
wf
,
atom-free-decl
wf
origin
A:MsgA. AtomFree(ds(A)) 
(x:Id. AtomFree(Type;A.ds(x))) A:MsgA. AtomFree(ds(A)) (x:Id. AtomFree(Type;A.ds(x))) Qx:A. B(x)
T
B(a)xdom(f). v=f(x) P(x;v)
B(x)
B
A
B(x)
x.A(x)
x. t(x)